es:event_system{i:l}, x:Id, e:es-E(es).
(es-isconst(es; loc(e); x))
 guard((constant_function(es-state-ap(es_state_when(es; e); x);
 guard((constant_function(rationals;
 guard((constant_function(es-vartype(es; loc(e); x))
 guard( constant_function(es-state-ap(es_state_after(es; e); x);
 guard( constant_function(rationals;
 guard( constant_function(es-vartype(es; loc(e); x)))) 

latex

Definitions	t  T, constant_function(f; A; B), x:A. B(x)
Lemmas	rationals wf, es time wf, qadd wf